Skip to content

Error handling cleanup in solvers/flattening 5 #2938

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 4 commits into from
Sep 26, 2018
Merged

Error handling cleanup in solvers/flattening 5 #2938

merged 4 commits into from
Sep 26, 2018

Conversation

danpoe
Copy link
Contributor

@danpoe danpoe commented Sep 12, 2018 •
edited
Loading

No description provided.

danpoe
danpoe commented Sep 12, 2018
View reviewed changes
src/solvers/flattening/boolbv_unary_minus.cpp Outdated

bvtypet bvtype=get_bvtype(type);
bvtypet op_bvtype=get_bvtype(op0.type());
std::size_t op_width=op_bv.size();
bvtypet op_bvtype = get_bvtype(op.type());

bool no_overflow=(expr.id()=="no-overflow-unary-minus");
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"no-overflow-unary-minus" does not seem to be assigned anywhere. Is this still needed?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@peterschrammel Do you know if we can remove "no-overflow-unary-minus"?

allredj
allredj reviewed Sep 12, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: baec7a1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84576476

@danpoe danpoe mentioned this pull request Sep 12, 2018
Merged
peterschrammel
peterschrammel reviewed Sep 17, 2018
View reviewed changes
src/solvers/flattening/boolbv_unary_minus.cpp Outdated
@@ -96,7 +85,7 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
}
else if(bvtype==bvtypet::IS_FLOAT && op_bvtype==bvtypet::IS_FLOAT)
{
assert(!no_overflow);
INVARIANT(!no_overflow, "");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

missing message

tautschnig
tautschnig reviewed Sep 21, 2018
View reviewed changes
src/solvers/flattening/boolbv_unary_minus.cpp

bvt tmp_result;
const auto sub_it = std::next(op_bv.begin(), sub_idx);
std::copy_n(sub_it, sub_width, std::back_inserter(tmp_op));
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm sure this is a good idea, but seems unrelated to the goal of the commit?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, this has become a separate commit now.

@danpoe danpoe force-pushed the refactor/error-handling-solvers-flattening-from-boolbv-unary-minus branch 5 times, most recently from f59eb53 to a86fbea Compare September 24, 2018 11:54
tautschnig
tautschnig requested changes Sep 24, 2018
View reviewed changes
Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Failing unit test:
java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp:17 with

Invariant check failed
File: std_types.h:1319 function: validate_type
Condition: signed bitvector type must have non-zero width
Reason: type.get_width() > 0

@danpoe danpoe force-pushed the refactor/error-handling-solvers-flattening-from-boolbv-unary-minus branch from a86fbea to 8c31e83 Compare September 25, 2018 14:15
@danpoe danpoe force-pushed the refactor/error-handling-solvers-flattening-from-boolbv-unary-minus branch from 8c31e83 to 7d629c5 Compare September 26, 2018 14:51
@danpoe
Copy link
Contributor Author

danpoe commented Sep 26, 2018

@tautschnig I've removed those additional checks type.get_width() > 0 now. Turns out zero-width bitvector types can legally appear due to e.g. 0-width members of bitfields.

@tautschnig tautschnig merged commit 03126ae into diffblue:develop Sep 26, 2018
allredj
allredj reviewed Sep 26, 2018
View reviewed changes
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Passed Diffblue compatibility checks (cbmc commit: 7d629c5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/86032809

@danpoe danpoe deleted the refactor/error-handling-solvers-flattening-from-boolbv-unary-minus branch June 2, 2020 17:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel left review comments

@allredj allredj allredj left review comments

@tautschnig tautschnig tautschnig approved these changes

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@martin-cs martin-cs Awaiting requested review from martin-cs martin-cs is a code owner

@pkesseli pkesseli Awaiting requested review from pkesseli

@smowton smowton Awaiting requested review from smowton

Assignees

@danpoe danpoe

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@danpoe @tautschnig @peterschrammel @allredj